package ch.epfl.lara.matcheck;

object Config {
  
  // Prover Config
  var PROVER: ch.epfl.lara.matcheck.verify.provers.TheoremProvers.Prover = _
  var PROVER_EXEC: String = _                           // The name of the executable 
  var PROVER_OPTIONS: String = _ 
  
  
  def verbose {
    Report.verbose("Prover: "+PROVER.toString)
    Report.verbose("Executable: "+PROVER_EXEC)
    Report.verbose("Options: "+PROVER_OPTIONS)
    Report.verbose("")
  }
  
  
  // Matcheck Config
  var DEBUG   : Boolean = _
  var WARNINGS: Boolean = _
  var VERBOSE : Boolean = _
  
  var PERFORMANCE: Boolean = _
  var STATS: Boolean = _
  
  var NOCHECKS: Boolean = false
  
  var NOSPEC: Boolean = _
  
  var HELP: Boolean  = _
  
  // checkable PM property 
  var COMPLETE : Boolean = true         // default: check completeness
  var DISJOINT : Boolean = _
  var REACHABLE: Boolean = _
}
